#include "ksat.h"

/* restriction of the strong inhibition model */
void sim_model (int N0, int N, int L, int S[L][3 * N], int g[N][N], int r[N][N], struct ksat *ksat)
{
	int i, j, k, t;
	int X1[L], X2[L], Z1[L][N], Z2[L][N]; /* temporary variable */
	int N_var1, base, list[N + 1];

	N_var1 = 2 * L + 2 * N * L;
	ksat->num_variables -= N_var1 * N0;
	base = ksat->num_variables;

	for (i = 0; i < L; i++)
	{
		X1[i] = i;
		X2[i] = L + i;
	}

	for (i = 0; i < L; i++)
	{
		for (j = 0; j < N; j++)
		{
			Z1[i][j] = 2 * L + i * N + j;
			Z2[i][j] = 2 * L + N * L + i * N + j;
		}
	}

	/* restriction of our Strong Inhibition Model */
	for (i = N0; i < N; i++)
	{
		for (t = 0; t < L; t++)
		{
			list[0] =  S[t][N + i]; list[1] =  base + N_var1 * i + X1[t]; list[2] =  base + N_var1 * i + X2[t];
			add_clause (ksat, 3, list);

			for (j = 0; j < N; j++)
			{
				list[0] =  S[t][N + i]; list[1] = -(base + N_var1 * i + X1[t]); list[2] = -S[t][j];
				if (i == j)
					list[3] =  r[i][j];
				else
					list[3] = -g[i][j];
				add_clause (ksat, 4, list);
			}

			list[0] =  S[t][N + i];
			for (j = 0; j < N; j++)
			{
				if (j == i)
					list[j + 1] = -(base + N_var1 * i + X2[t]);
				else
					list[j + 1] =  base + N_var1 * i + Z1[t][j];
			}
			add_clause (ksat, N + 1, list);

			for (j = 0; j < N; j++)
			{
				if (j == i) continue;

				list[0] =  S[t][N + i]; list[1] = -(base + N_var1 * i + X2[t]); list[2] = -(base + N_var1 * i + Z1[t][j]); list[3] =  S[t][j];
				add_clause (ksat, 4, list);

				list[0] =  S[t][N + i]; list[1] = -(base + N_var1 * i + X2[t]); list[2] = -(base + N_var1 * i + Z1[t][j]); list[3] =  r[i][j];
				add_clause (ksat, 4, list);
			}

			list[0] = -S[t][N + i];
			for (j = 0; j < N; j++)
			{
				list[j + 1] = base + N_var1 * i + Z2[t][j];
			}
			add_clause (ksat, N + 1, list);

			for (j = 0; j < N; j++)
			{
				list[0] = -S[t][N + i]; list[1] = -(base + N_var1 * i + Z2[t][j]); list[2] =  S[t][j];
				add_clause (ksat, 3, list);

				list[0] = -S[t][N + i]; list[1] = -(base + N_var1 * i + Z2[t][j]);
				if (i == j)
					list[2] = -r[i][j];
				else
					list[2] =  g[i][j];
				add_clause (ksat, 3, list);
			}

			for (j = 0; j < N; j++)
			{
				if (j == i) continue;

				list[0] = -S[t][N + i]; list[1] = -S[t][j]; list[2] = -r[i][j];
				add_clause (ksat, 3, list);
			}
		}
	}

	ksat->num_variables += N_var1 * N;
}

/* restriction of no quick flips */
void forbidden_quickflips (int N0, int N, int L, int S[L][N], struct ksat *ksat)
{
	int i, j, list[3];

	for (i = 0; i < L - 3; i++)
	{
		for (j = N0; j < N; j++)
		{
			list[0] =  S[i][j]; list[1] = -S[i + 1][j]; list[2] =  S[i + 2][j];
			add_clause (ksat, 3, list);

			list[0] = -S[i][j]; list[1] =  S[i + 1][j]; list[2] = -S[i + 2][j];
			add_clause (ksat, 3, list);
		}
	}
}

/* restriction of reliable transisition */
void reliable_trans (int N0, int N, int L, int S[L][3 * N], int g[N][N], int r[N][N], struct ksat *ksat)
{
	int i, j, k, t, n0;
	int X[L][N], Y[L][N]; /* temporary variable */
	int N_var, base, list[N + 2];

	N_var = 2 * N * L;
	ksat->num_variables -= N_var * N0;
	base = ksat->num_variables;

	for (i = 0; i < L; i++)
	{
		for (j = 0; j < N; j++)
		{
			X[i][j] = i * N + j;
			Y[i][j] = N * L + i * N + j;
		}
	}

	for (i = N0; i < N; i++)
	{
		for (t = 0; t < L; t++)
		{
			if (N0 > 0 && t > 0)
				n0 = 1;
			else
				n0 = 0;

			list[0] =  S[t][i];
			for (j = n0; j < N; j++)
			{
				if (i == j)
					list[j + 1 - n0] = -S[t][N + i];
				else
					list[j + 1 - n0] =  base + N_var * i + X[t][j];
			}
			add_clause (ksat, N + 1 - n0, list);

			for (j = n0; j < N; j++)
			{
				if (i == j)
					continue;

				list[0] =  S[t][i]; list[1] = -S[t][N + i]; list[2] = -(base + N_var * i + X[t][j]); list[3] =  S[t][j];
				add_clause (ksat, 4, list);

				list[0] =  S[t][i]; list[1] = -S[t][N + i]; list[2] = -(base + N_var * i + X[t][j]); list[3] =  S[t][N + j];
				add_clause (ksat, 4, list);

				list[0] =  S[t][i]; list[1] = -S[t][N + i]; list[2] = -(base + N_var * i + X[t][j]); list[3] =  g[i][j];
				add_clause (ksat, 4, list);

				list[0] =  S[t][i]; list[1] = -S[t][N + i]; list[2] = -S[t][j]; list[3] = -r[i][j];
				add_clause (ksat, 4, list);

				list[0] =  S[t][i]; list[1] = -S[t][N + i]; list[2] = -S[t][N + j]; list[3] = -r[i][j];
				add_clause (ksat, 4, list);
			}

			/*************************************************/

			list[0] = -S[t][i]; list[1] =  S[t][N + i]; list[2] = -(base + N_var * i + Y[t][i]); list[3] =  r[i][i];
			add_clause (ksat, 4, list);

			list[0] = -S[t][i]; list[1] =  S[t][N + i];
			for (j = n0; j < N; j++)
				list[j + 2 - n0] = base + N_var * i + Y[t][j];
			add_clause (ksat, N + 2 - n0, list);

			for (j = n0; j < N; j++)
			{
				if (i == j)
					continue;

				list[0] = -S[t][i]; list[1] =  S[t][N + i]; list[2] = -(base + N_var * i + Y[t][i]); list[3] = -S[t][j]; list[4] = -g[i][j];
				add_clause (ksat, 5, list);

				list[0] = -S[t][i]; list[1] =  S[t][N + i]; list[2] = -(base + N_var * i + Y[t][i]); list[3] = -S[t][N + j]; list[4] = -g[i][j];
				add_clause (ksat, 5, list);

				list[0] = -S[t][i]; list[1] =  S[t][N + i]; list[2] = -(base + N_var * i + Y[t][j]); list[3] =  S[t][j];
				add_clause (ksat, 4, list);

				list[0] = -S[t][i]; list[1] =  S[t][N + i]; list[2] = -(base + N_var * i + Y[t][j]); list[3] =  S[t][N + j];
				add_clause (ksat, 4, list);

				list[0] = -S[t][i]; list[1] =  S[t][N + i]; list[2] = -(base + N_var * i + Y[t][j]); list[3] =  r[i][j];
				add_clause (ksat, 4, list);
			}
		}
	}

	ksat->num_variables += N_var * N;
}

/* restriction of convergence */
void convergence (int N0, int N, int L, int S[L][3 * N], int g[N][N], int r[N][N], struct ksat *ksat)
{
	int i, j, k, t, n0;
	int X[L][N], Y[L][N]; /* temporary variable */
	int N_var, base, list[N + 2];

	N_var = 2 * N * L;
	ksat->num_variables -= N_var * N0;
	base = ksat->num_variables;

	for (i = 0; i < L; i++)
	{
		for (j = 0; j < N; j++)
		{
			X[i][j] = i * N + j;
			Y[i][j] = N * L + i * N + j;
		}
	}

	for (i = N0; i < N; i++)
	{
		for (t = 0; t < L; t++)
		{
			if (N0 > 0 && t > 0)
				n0 = 1;
			else
				n0 = 0;

			list[0] = -(base + N_var * i + X[t][i]); list[1] =  S[t][i];
			add_clause (ksat, 2, list);

			list[0] = -(base + N_var * i + X[t][i]); list[1] = -r[i][i];
			add_clause (ksat, 2, list);

			list[0] = -S[t][N + i]; list[1] = -S[t][2 * N + i];
			for (j = n0; j < N; j++)
				list[j + 2 - n0] = base + N_var * i + X[t][j];
			add_clause (ksat, N + 2 - n0, list);

			for (j = n0; j < N; j++)
			{
				if (i == j)
					continue;

				list[0] = -S[t][N + i]; list[1] = -S[t][2 * N + i]; list[2] = -(base + N_var * i + X[t][j]); list[3] =  S[t][j];
				add_clause (ksat, 4, list);

				list[0] = -S[t][N + i]; list[1] = -S[t][2 * N + i]; list[2] = -(base + N_var * i + X[t][j]); list[3] =  S[t][N + j];
				add_clause (ksat, 4, list);

				list[0] = -S[t][N + i]; list[1] = -S[t][2 * N + i]; list[2] = -(base + N_var * i + X[t][j]); list[3] =  g[i][j];
				add_clause (ksat, 4, list);

				list[0] = -S[t][N + i]; list[1] = -S[t][2 * N + i]; list[2] = -S[t][j]; list[3] = -r[i][j];
				add_clause (ksat, 4, list);

				list[0] = -S[t][N + i]; list[1] = -S[t][2 * N + i]; list[2] = -S[t][N + j]; list[3] = -r[i][j];
				add_clause (ksat, 4, list);
			}

			/*************************************************/

			list[0] =  S[t][N + i]; list[1] =  S[t][2 * N + i]; list[2] = -(base + N_var * i + Y[t][i]); list[3] =  r[i][i]; list[4] = -S[t][i];
			add_clause (ksat, 5, list);

			list[0] =  S[t][N + i]; list[1] =  S[t][2 * N + i];
			for (j = n0; j < N; j++)
				list[j + 2 - n0] = base + N_var * i + Y[t][j];
			add_clause (ksat, N + 2 - n0, list);

			for (j = n0; j < N; j++)
			{
				if (i == j)
					continue;

				list[0] =  S[t][N + i]; list[1] =  S[t][2 * N + i]; list[2] = -(base + N_var * i + Y[t][i]); list[3] = -S[t][j]; list[4] = -g[i][j];
				add_clause (ksat, 5, list);

				list[0] =  S[t][N + i]; list[1] =  S[t][2 * N + i]; list[2] = -(base + N_var * i + Y[t][i]); list[3] = -S[t][N + j]; list[4] = -g[i][j];
				add_clause (ksat, 5, list);

				list[0] =  S[t][N + i]; list[1] =  S[t][2 * N + i]; list[2] = -(base + N_var * i + Y[t][j]); list[3] =  S[t][j];
				add_clause (ksat, 4, list);

				list[0] =  S[t][N + i]; list[1] =  S[t][2 * N + i]; list[2] = -(base + N_var * i + Y[t][j]); list[3] =  S[t][N + j];
				add_clause (ksat, 4, list);

				list[0] =  S[t][N + i]; list[1] =  S[t][2 * N + i]; list[2] = -(base + N_var * i + Y[t][j]); list[3] =  r[i][j];
				add_clause (ksat, 4, list);
			}
		}
	}

	ksat->num_variables += N_var * N;
}
